Require Import ZArith.
Open Scope Z_scope.

Notation int := nat.

Inductive ty_hp:Set :=
  | ty_Int:  ty_hp
  | ty_Bool: ty_hp
  | ty_Void: ty_hp
  | ty_Str: int -> ty_hp (* struct (id) *) 
  | ty_Pt: ty_hp -> ty_hp   (* pointer (ty)*)
  | ty_Array: nat -> ty_hp -> ty_hp. (* array(i, ty) *)

Inductive value :Set :=
  | Int: Z -> value
  | Bool : bool -> value
  | Tyhp : ty_hp -> value.

Definition heap:Set := ty_hp -> Z -> value.

Definition sel(h:heap)(ty:ty_hp)(a:Z):value := h ty a.
Definition upd(h:heap)(ty:ty_hp)(a:Z)(v:value):ty_hp->Z->value := fun (ty:ty_hp)(a1:Z) =>
  if (Zeq_bool a a1) then v else (h ty a1).

Axiom w1: forall h ty a v, sel (upd h ty a v) ty a = v.

Axiom w2: forall h ty a a1 v, a<>a1 ->  sel (upd h ty a v) ty a1 = h ty a1. 